//*****************************************************************************/
//* Copyright (C) 2005-2013                                                   */
//* MEL O'CAT  X178G243 (at) yahoo (dot) com                                  */
//* License terms: GNU General Public License Version 2                       */
//*                or any later version                                       */
//*****************************************************************************/
//*456789012345678 (80-character line to adjust editor window) 456789012345678*/

/*
 * MinGeneratedProofStmt.java  0.01 11/01/2011
 *
 * Version 0.01:
 * Nov-01-2011: new.
 */

package mmj.gmff;

/**
 * General object representing a Generated Proof statement on a
 * {@code MinProofWorksheet}.
 * <p>
 * Generated Proof statements are generated by mmj2 Proof Assistant when the
 * user presses Ctrl-U (Unify) and unification successfully creates a Metamath
 * proof -- which is simply a RPN (Reverse Polish Notation) list of Metamath
 * statement labels. The Generated Proof statement consists of "$=" in column 1
 * of the first line of the Generated Proof statement followed by the
 * space-separated list of statement labels.
 * <p>
 * Nothing is typeset by GMFF, and the labels are output as if they were just
 * text, or comments (unlike the Metamath Proof Explorere web pages which
 * contain hyperlinks for the statement labels.)
 */
public class MinGeneratedProofStmt extends MinProofWorkStmt {

    /**
     * Standard MinGeneratedProofStmt constructor.
     * 
     * @param w {@code MinProofWorksheet} of which this statement is a part.
     * @param slc Array of Array of String representing the lines and "chunks"
     *            making up the {@code MinProofWorkStmt}.
     */
    public MinGeneratedProofStmt(final MinProofWorksheet w, final String[][] slc)
    {

        super(w, slc);
    }

    /**
     * Formats export data for the Generated Proof statement according to the
     * {@code Model A} specifications and loads the data into a specified
     * buffer.
     * <p>
     * Model A model files for {@code MinGeneratedProofStmt} objects are
     * "optional", meaning that if any of the model files are not found, the
     * export process is continues normally but Generated Proof statements are
     * not output as part of the Proof Worksheet export.
     * <p>
     * Note the quirky handling of {@code modelAGenProof1X}. If this model file
     * is empty then no data is output at that location. This quirky feature
     * will generally not be used but is provided for maximum flexibility in
     * creating export format models.
     * <p>
     * Additional information may be found \GMFFDoc\GMFFModels.txt.
     * 
     * @param gmffExporter The {@code GMFFExporter} requesting the export data
     *            build.
     * @param exportBuffer The {@code StringBuilder} to which exported data is
     *            to be output.
     * @throws GMFFException if errors are encountered during the export
     *             process.
     */
    @Override
    public void buildModelAExport(final GMFFExporter gmffExporter,
        final StringBuilder exportBuffer) throws GMFFException
    {

        final String modelAGenProof0 = gmffExporter
            .getOptionalModelFile(GMFFConstants.MODEL_A_GENPROOF0_NAME);
        if (modelAGenProof0 == null)
            return;

        final String modelAGenProof1X = gmffExporter
            .getOptionalModelFile(GMFFConstants.MODEL_A_GENPROOF1X_NAME);
        if (modelAGenProof1X == null)
            return;
        final String modelAGenProof2 = gmffExporter
            .getOptionalModelFile(GMFFConstants.MODEL_A_GENPROOF2_NAME);
        if (modelAGenProof2 == null)
            return;

        // well all righty then...

        for (int i = 0; i < stmtLineChunks.length; i++) {

            gmffExporter.appendModelFileText(exportBuffer, modelAGenProof0);

            if (modelAGenProof1X.length() > 0)
                gmffExporter.escapeAndAppendProofText(exportBuffer,
                    getCleanedLineString(i));

            gmffExporter.appendModelFileText(exportBuffer, modelAGenProof2);
        }
    }
}
